\begin{tabbing}
master{-}antecedent\{i:l\}(${\it es}$;${\it Cmd}$;${\it Master}$;${\it Config}$;${\it Sys}$;$m$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:\{$e$:E(${\it Master}$)$\mid$ $\uparrow$cmseq?(${\it Master}$($e$))\} . ($m$($e$) $<$ $e$))\+
\\[0ex]\& ($\forall$$e_{1}$, $e_{2}$:\{$e$:E(${\it Master}$)$\mid$ $\uparrow$cmseq?(${\it Master}$($e$))\} . ($m$($e_{1}$) $<$loc $m$($e_{2}$)) $\Rightarrow$ ($e_{1}$ $<$ $e_{2}$))
\\[0ex]\& (\=$\forall$$e$:\{$e$:E(${\it Master}$)$\mid$ $\uparrow$cmseq?(${\it Master}$($e$))\} .\+
\\[0ex]let \=$c$\= = ${\it Config}$($m$($e$)) in\+\+
\\[0ex]($\uparrow$ccpred?($c$))
\-\\[0ex]\& ccpred{-}id($c$) = cmseq{-}to(${\it Master}$($e$))
\\[0ex]\& loc($m$($e$)) = cmseq{-}from(${\it Master}$($e$))
\\[0ex]\& $\parallel$cmd{-}history($m$($e$))$\parallel$ = cmseq{-}num(${\it Master}$($e$)))
\-\-\-
\end{tabbing}